(include-book "doublecheck" :dir :teachpacks)
(include-book "list-utilities" :dir :teachpacks)

;helper function for property tests
;and distribution generators.
;Takes a list of lists and returns one list
;of all the lists appended together in order.
(defun append-all (xss)
  (if (consp xss)
      (append (car xss) (append-all (cdr xss)))
      nil))

;generate a random character that isn't <, > or 
;whitespace
(defrandom random-xml-char ()
  (let* ((chr (random-char)))
    (if (member-equal chr
                      (list #\return #\newline 
                          #\tab #\space #\<
                          #\>))       
        #\x
        chr)))

(defrandom random-xml-chars ()
  (random-list-of (random-xml-char)))

;;generate an XML start tag with
;;chrs as its name
(defun to-xml-tag (chrs)
  (append '( #\<) chrs '( #\>)))

;;generate an xml closing tag
;;with chrs as its name
(defun to-end-tag (chrs)
   (append '( #\< #\/) chrs '( #\>)))

;;generate a random XML element with
;;the given max depth. The mechanism for
;;avoiding infinite recursion used here was
;;borrowed from the random-expression example
;;on http://planet.plt-scheme.org/package-source/cce/dracula.plt/4/0/planet-docs/manual/_doublecheck_.html
(defrandom random-xml (max-depth)
  (append
     (to-xml-tag (random-xml-chars))
     (random-case 
        (random-xml-chars) ;trivial XML element
        (append-all (random-list-of (random-xml (1- max-depth)))) ;add some
                                                     ;recursive entries
        :weight (- 1 (/ 1 max-depth))) ;drop probability of recursing
                                       ;as you go deeper, to avoid
                                       ;infinite recursion
     (to-end-tag (random-xml-chars))))




;;Tests that parse-xml-tag returns two elements:
;; the value of the tag and the text after the tag.
(defproperty parse-xml-tag-parses-tag-and-leaves-rest
  (tag-value :value (random-list-of (random-xml-char))
   rest :value (random-list-of (random-char)))
  (equal (parse-tag (append (to-xml-tag tag-value) rest))
         (list tag-value rest)))

;;Tests that parse-end-tag returns its input with
;;the end tag at the beginning removed.
(defproperty parse-end-tag-skips-only-tag
   (tag-value :value (random-xml-chars)
   rest :value (random-list-of (random-char)))
  (equal (parse-end-tag (append (to-end-tag tag-value) rest))
         rest))

;;checks that parse-body works correctly on
;;a list of characters that begins with a
;;body that is just an atom, not another
;;XML element. It should return the body
;;as a string, and stuff after the end tag
;;as a list of characters (for further parsing)
(defproperty parsing-trivial-body-returns-string-body-and-remainder
  (body :value (random-xml-chars)
   end :value (to-end-tag (random-xml-chars))
   rest :value (random-list-of (random-char)))
  (equal (parse-body (append body end rest))
         (list (chrs->str body) (append end rest))))


 
(include-book "testing" :dir :teachpacks)

;;consts used in a check-expect for essentially the same
;;thing as the parsing-xml-returns-matching-item test below.
;;I wrote this for debugging and decided to keep it because
;;it has value as a demonstration.
(defconst *tn* "abba")
(defconst *xml* "<text><s>df</s><b><m>fdb</m><m>fdf</m></b></text><sss></sss>")
(defconst *rest* "qqqqqqq")
(defconst *all* (append (to-xml-tag (str->chrs *tn*)) (str->chrs *xml*) (to-end-tag (str->chrs *tn*)) (str->chrs *rest*)))


(check-expect (parse-xml *all*) (list (list *tn* (car (parse-body (str->chrs *xml*)))) (str->chrs *rest*)))

;;This tests that a call to parse-xml correctly parses
;;the outer layer of the XML. Since parse-xml will end up
;;calling itself recursively for more complicated XML structures,
;;this tests a critical correctness property 
;;(though it doesn't ensure correctness)
;;
;;The expected element is a list whose first element
;;is the parse results:
;;  A list of two elements containing the tag name as a string,
;;  followed by the value returned by calling parse-xml
;;  on its inner text.
;;and whose second element is the remainder of the character
;;list
(defproperty parsing-xml-returns-matching-item
  (tag-name :value (random-xml-chars)
   body :value (random-xml-chars)
   rest :value (random-list-of (random-char)))
  (let* ((chrs (append (to-xml-tag tag-name)
                       body
                       (to-end-tag tag-name)
                       rest)))
    (equal (parse-xml chrs)
           (list (list (chrs->str tag-name) (car (parse-body body)))
                 rest))))


 
;;This test takes a "document" composed of a random list of
;;random XML elements, and ensures that the output matches
;;the results of a list created by parsing each XML element.
;;
;;Note that this doesn't guarantee parse-xml-doc's correctness
;;without assuming the correctness of parse-xml; that's why
;;the above tests are needed to make a case for parse-xml's
;;correctness.
(defproperty parsing-full-xml-document-returns-list-of-xml-elems-as-alist
  (xml-elems-as-chrs :value (cons (random-xml 10) (random-list-of (random-xml 10)))
   index :value (mod (random-natural) (len xml-elems-as-chrs)))
  (equal (nth index (parse-xml-doc (append-all xml-elems-as-chrs)))
         (car (parse-xml (nth index xml-elems-as-chrs)))))